A,B:es_realizer{i:l}. R-interface-compat(A; B)  prop{i:l} 

latex

Definitions	x. t(x), ff, t.2, outl(x), t.1, isl(x), tt, P  Q, tag(k), lnk(k), isrcv(k), band(p; q), let x = a in b(x), if b then t else f fi , R-interface-compat(A; B), prop{i:l}, t  T, x:A. B(x), x(s), Knd, P  Q, P  Q, Unit, , , locl(a), rcv(l,tg)
Lemmas	es realizer wf, Rsends-T wf, Rsends-knd wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Reffect-T wf, id-deq wf, Rsends-dt wf, Id wf, fpf-cap wf, subtype rel wf, Rsends-l wf, eq lnk wf, ifthenelse wf, Reffect-knd wf, true wf, Reffect? wf, eqtt to assert, bool wf, Rsends? wf